The development of complex high-assurance platforms for commercial and military control systems, such as avionics and communications, and secure computing applications such as crypto modernization, guard applications and Multiple Independent Levels of Security (MILS) separation has generated a need for an efficient development and certification path for such high-assurance systems. To date, traditional approaches to the development and verification of microcode (also known as microprograms or firmware) for microprocessors have been labor intensive, error prone, and have lacked a formal specification for their implementation.
Such approaches have been based on textual specifications and implemented by hand-coding. Hand-coding is a labor intensive task requiring an individual intimately familiar with both the target architecture and the behavioral specifications of the desired microprogram. Verification has been performed through simulations which are driven by hand-generated test cases, corner case stimulus, or random input stimulus.
Further complicating this approach is the development of the simulation environment itself. In most cases, the development of the target microprocessor architecture (and the associated simulation platform) is a parallel effort with that of the development of the microcode. The simulation platform must be accurate at the gate and clock-cycle level to provide the microprogrammer with a faithful simulation tool. In order to accurately model register and gate level architecture of the target platform, the choice of simulation environments is often between a hardware description language (HDL) simulator intended for hardware development and a proprietary hand-coded software based simulator. Hand-coded software based simulators are oftentimes the preferred option as they may be specifically tailored to meet the needs of a microprogrammer.
To develop and certify high-assurance microcode, traditional approaches are inadequate due to the possibility of errors in specification interpretation, hand coding and incomplete test case coverage. In addition, the development time and cost associated with the simulation environment development may also be significant.
Achieving the Common Criteria for certain Evaluation Assurance Levels (EAL) requires the use of semi-formal or formal certification tools. For example, EAL 5 and 6 require semi-formal analysis while EAL 7 requires full formal analysis. Traditional approaches to microcoding fail to address these aspects of certification.
In addition, the artifacts and proofs of correctness necessary for the rigorous nature of high-assurance certification are not inherent to the development process and must be generated at the end of the design cycle.
As such, there is a need for efficient methods and systems for the development of certifiable high-assurance microcode which integrates current model-based design principles with automatic code generation of microcode and associated test cases, and automated analysis tools, such as model checkers and theorem provers. Such methods and systems provide designs having a documented pedigree of correctness.